|
|
An Automatic Theorem Prover
Mazánek, Martin ; Havlena, Vojtěch (referee) ; Lengál, Ondřej (advisor)
This thesis focuses on implementation of resolution-based automatic theorem prover for propositional and first-order logic. The goal of this thesis is to create simple prover and document the development. Making state-of-the-art prover is not the goal of this thesis. We also present some popular automated theorem provers.
|
|
|
Implementation of the mandate of the UNPROFOR mission in Bosnia and Herzegovina between 1992-1995
Lalić, Jan ; Tejchman, Miroslav (advisor) ; Pikal, Kamil (referee)
The unwillingness of the international community to become involved militarily in Bosnian civil war between 1992-1995, made the United Nations Protection Force (UNPROFOR) a substitute for a decisive action. The absence of any foreseeable prospect of truce, which would have been supported by the presence of peacekeepers, led to the establishment of strictly humanitarian mandate for UN troops in the first phase of the war. They were supposed, in cooperation with the United Nations High Commisioner for Refugees (UNHCR), to secure functioning of the Sarajevo airport for humanitarian relief purposes and subsequently provide security for the UNHCR and its convoys providing humanitarian relief. Thesis "Implementation of the mandate of the UNPROFOR mission in Bosnia and Herzegovina between 1992-1995" deals with issues concerning humanitarian mandate in particular. This thesis aims to explain, through descriptive analysis, motives leading international community to deploy lightely armed peacekeeprs with uncharacteristic mandate to the region, which is absolutely inadequate for peacekeeping operations as I will show. It will subsequently analyze course of the implementation and problems, which were encountered by UN troops. The aim of this thesis is to prove, that UNPROFOR was not absolute failure as it is perceived,...
|
|
|
Finding Minimum Satisfying Assignments of Boolean Formulas
Švancara, Jiří ; Balyo, Tomáš (advisor) ; Trunda, Otakar (referee)
In this thesis we examine algorithms and techniques used for solving Boolean satisfiability (SAT). Then we inspect the possibility to use them in solving the weighted short SAT problem, which is a generalization of the satisfiability problem. Given that each variable has a weight, this generalization is the problem of finding a satisfying truth assignment while using the smallest sum of weights. To solve this problem, we introduce three truth assignments of variables - True, False and Unassign. We show that not all algorithms and techniques used in modern SAT solvers can be used in our program. Those that can be converted, will be implemented using our three truth assignments. This will yield several versions of our new solver, which will be compared. Powered by TCPDF (www.tcpdf.org)
|
|
|
On the Power of Weak Extensions of V0
Müller, Sebastian Peter ; Krajíček, Jan (advisor) ; Thapen, Neil (referee) ; Kolodziejczyk, Leszek (referee)
Název práce: O síle slabých rozšírení teorie V0 Autor: Sebastian Müller Katedra: Katedra Algebry Vedoucí disertační práce: Prof. RNDr. Jan Krajíček, DrSc., Katedra Algebry. Abstrakt: V predložené disertacní práci zkoumáme sílu slabých fragmentu arit- metiky. Činíme tak jak z modelově-teoretického pohledu, tak z pohledu důkazové složitosti. Pohled skrze teorii modelu naznačuje, že malý iniciální segment libo- volného modelu omezené aritmetiky bude modelem silnější teorie. Jako příklad ukážeme, že každý polylogaritmický řez modelu V0 je modelem VNC. Užitím známé souvislosti mezi fragmenty omezené aritmetiky a dokazatelností v ro- zličných důkazových systémech dokážeme separaci mezi rezolucí a TC0 -Frege systémem na náhodných 3CNF-formulích s jistým poměrem počtu klauzulí vůci počtu proměnných. Zkombinováním obou výsledků dostaneme slabší separační výsledek pro rezoluci a Fregeho důkazové systémy omezené hloubky. Klíčová slova: omezená aritmetika, důkazová složitost, Fregeho důkazový systém, Fregeho důkazový systém omezené hloubky, rezoluce Title: On the Power of Weak Extensions of V0 Author: Sebastian Müller Department: Department of Algebra Supervisor: Prof. RNDr. Jan Krajíček, DrSc., Department of Algebra....
|
|
|
Importance of United Nations Security Council and binding effect of resolutions in maintenance of international peace and security
Urbanová, Petra ; Ondřej, Jan (advisor) ; Balaš, Vladimír (referee)
- Importance of United Nations Security Council and binding effect of resolutions in maintenance of international peace and security This paper depicts the history previous to creation and the creation itself of UN and the Security Council, followed by chapter devoted to the permanent and non- permanent members of the Council with subchapter about reform proposals in terms of its composition. Then there is detailed description of functions and powers of the Security Council, including also a topic relating to the Council's period of paralysis. In the chapter on voting procedure there is stressed the crucial issue of distinguishing procedural and non-procedural resolutions with talking about veto power as well. The final chapter is devoted to the decisions of the Security Council with focus on resolutions and their binding effect.
|
|
|
An Automatic Theorem Prover
Mazánek, Martin ; Havlena, Vojtěch (referee) ; Lengál, Ondřej (advisor)
This thesis focuses on implementation of resolution-based automatic theorem prover for propositional and first-order logic. The goal of this thesis is to create simple prover and document the development. Making state-of-the-art prover is not the goal of this thesis. We also present some popular automated theorem provers.
|
|
|
The Resolution Fund: Is behaviour of the contributing institutions affected by the applied methodology?
Hykl, Daniel ; Pečená, Magda (advisor) ; Džmuráňová, Hana (referee)
Daniel Hykl Bachelor Thesis The Resolution Fund: Is behaviour of the contributing institutions affected by the applied methodology? Abstract The thesis provides theoretical analysis of the Resolution Fund contributions determination policy - the contributions are calculated based on end of year data - and its effects on banks and the financial sector. Several theoretical examples are used to demonstrate the problem of the top-down approach to distribution of the sectoral contributions on the particular institutions. A hypothesis is drawn - do the banks lower their reported liabilities as of end of the year to achieve decreased contributions? Total liabilities of the 7 largest banks in the Czech Republic are analysed and theoretical end of year developments of total liabilities of the banks under no optimisation condition are calculated. Basic annual contributions of the banks are estimated and compared to implied contributions calculated from the theoretical liabilities.
|
|
|
Legality of the intervention during Yemeni Civil War
Hambálek, Jiří ; Bílková, Veronika (advisor) ; Ondřej, Jan (referee)
LEGALITY OF THE INTERVENTION DURING YEMENI CIVIL WAR Abstract The main purpose of this paper is to answer the questuion, if the Saudi Arabian-led intervention code-named operation Decisive Storm in Yemen during Yemeni civil war in 2015 was in accordance with the international law, precisely in accordance with the ius ad bellum. To achieve this purpose, the paper is divided into three parts. The first one, represented by chapters 1-6, describes self-defence, armed actions of the Security Council under the chap. VII of the UN Charter, intervention by invitation, concept of the humanitarian intervention and R2P concept. The role of regional arrangements in peacekeeping is also mentioned. The second part, represented by chap. 7, contains a case study whose object is the beginning of the Yemeni civil war at the turn of the year 2014and 2015 between president Hadi forces supported by the Saudi Arabian-led coalition and the Houthi rebels. The chapter 7 contains a detailed summary of various political decisions, UN Security Council resolutions, battles and campaigns, including the operation Decisive Storm. The third part, chap. 8, is pointed on the question of legality of the intervention. Albeit the invitation by president Hadi, the legality of the intervention was questioned. This chapter contains an analysis of...
|
|
|
The role of UNPROFOR peacekeepers during the war in Bosnia and Herzegovina focusing on the safe area Gorazde
Poláková, Michaela ; Žíla, Ondřej (advisor) ; Šístek, František (referee)
The goal of this thesis is to analyse the role of UNPROFOR (United Nations Protection Force) during the war in Bosnia and Herzegovina in the years 1993-1995. The deployment of a peace-keeping mission was the only step taken by the Western countries towards resolving the conflict in the beginning, because none of the states were willing to intervene militarily. The humanitarian mission was supposed to be a temporary solution to the crisis, with the sole purpose of easing the suffering of the civilian population. At first, the main goal of UNPROFOR was to secure and maintain the Sarajevo airport, which was used for delivering supplies. With the conflict continuing, the UNPROFOR mandate was expanded, e.g. to protection of the humanitarian convoys. An important moment for the international community came with the introduction of the safe area concept. First one was established around Srebrenica, then other five were created - Tuzla, Bihać, Gorazde, Zepa and Sarajevo. With the help of UNPROFOR, these enclaves were supposed to safeguard the civilians and secure access to basic needs. The aim of this project is to find specific reasons behind the unsuccessful UNPROFOR mission and to determine, whether it was the fault of the soldiers themselves or of the international community. The hypothesis this thesis...
|
|
|
Legality of the intervention during Libyan Civil War
Hambálek, Jiří ; Bílková, Veronika (advisor) ; Faix, Martin (referee)
LEGALITY OF THE INTERVENTION DURING LIBYAN CIVIL WAR Abstract The main purpose of this paper is to answer the questuion, if the NATO intervention in Libya during Libyan civil war in 2011 was in accordance with the international law. To achieve this purpose, the paper is divided into three parts. The first one, represented by chapters 1-5, describes self-defence and armed actions of the Security Council under the chap. VII of the UN Charter, which are legal and quite controversial concept of the humanitarian intervention and R2P concept. The role of regional arrangements in peacekeeping is also mentioned. The second part, represented by chap. 6, contains a case study whose object is the Libyan civil war in 2011 between col. Gaddafi's forces and the rebels supported by the NATO. The chapter 6 contains a detailed summary of various demonstrations, battles and campaigns, including the operation Unified Protector. The third part, chap. 7, is pointed on the question of legality of the NATO intervention. Albeit authorisation by the Resolution 1973, the legality of the intervention is questionable. The first air strikes, of 19 March, aimed on Libyan armed forces attacking Benghazi, can be classified as protection of civilians mentioned by the Resolution 1973. Following NATO air strikes supported the rebels in a...
|
guest ::
